Inference at * 
Iof proof for Lemma invert-union wf:


  A, B:Type, x:(A + B). invert-union(x)  (B + A) 

latex

 by (Unfolds ``invert-union`` ( 0)) 
CollapseTHEN (Auto) 

latex

C.

Definitions

invert-union(x), x:A. B(x), case b of inl(x) => s(x) | inr(y) => t(y), inr x , inl x , left + right, t  T, Type